/* @LICENSE(NICTA_CORE) */

#ifndef __LIBSEL4_ARCH_SYSCALLS_H
#define __LIBSEL4_ARCH_SYSCALLS_H

#include <stdint.h>

#define __SWINUM(x) ((x) & 0x00ffffff)

static inline void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysSend;
    asm volatile ("swi %[swi_num]"
            : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
              "+r" (msg3), "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysSend), "r"(scno)
            : "memory");
}

static inline void
__seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");
    register seL4_Word scno asm("r7") = seL4_SysSend;

    if (mr0 != NULL && msgInfo.length > 0) { msg0 = *mr0; }
    if (mr1 != NULL && msgInfo.length > 1) { msg1 = *mr1; }
    if (mr2 != NULL && msgInfo.length > 2) { msg2 = *mr2; }
    if (mr3 != NULL && msgInfo.length > 3) { msg3 = *mr3; }

    /* Perform the system call. */
    asm volatile ("swi %[swi_num]"
            : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
              "+r" (msg3), "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysSend), "r"(scno)
            : "memory");
}

static inline void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysNBSend;
    asm volatile ("swi %[swi_num]"
            : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
              "+r" (msg3), "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysNBSend), "r"(scno)
            : "memory");
}

static inline void
__seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");
    register seL4_Word scno asm("r7") = seL4_SysNBSend;

    if (mr0 != NULL && msgInfo.length > 0) { msg0 = *mr0; }
    if (mr1 != NULL && msgInfo.length > 1) { msg1 = *mr1; }
    if (mr2 != NULL && msgInfo.length > 2) { msg2 = *mr2; }
    if (mr3 != NULL && msgInfo.length > 3) { msg3 = *mr3; }

    /* Perform the system call. */
    asm volatile ("swi %[swi_num]"
            : "+r" (destptr), "+r" (msg0), "+r" (msg1), "+r" (msg2),
              "+r" (msg3), "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysNBSend), "r"(scno)
            : "memory");
}

static inline void
seL4_Reply(seL4_MessageInfo msgInfo)
{
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysReply;
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysReply), "r"(scno)
            : "memory");
}

static inline void
__seL4_ReplyWithMRs(seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word info asm("r1") = msgInfo.raw;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");
    register seL4_Word scno asm("r7") = seL4_SysReply;

    if (mr0 != NULL && msgInfo.length > 0) { msg0 = *mr0; }
    if (mr1 != NULL && msgInfo.length > 1) { msg1 = *mr1; }
    if (mr2 != NULL && msgInfo.length > 2) { msg2 = *mr2; }
    if (mr3 != NULL && msgInfo.length > 3) { msg3 = *mr3; }

    /* Perform the system call. */
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysReply), "r"(scno)
            : "memory");
}

static inline void
seL4_Notify(seL4_CPtr dest, seL4_Word msg)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_Word info asm("r1") = (seL4_MessageInfo){{ .length = 1 }}.raw;
    register seL4_Word msg0 asm("r2") = msg;

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysSend;
    asm volatile ("swi %[swi_num]"
            : "+r" (destptr), "+r" (msg0), "+r" (info)
            : [swi_num] "i" __SWINUM(seL4_SysSend), "r"(scno)
            : "memory");
}

static inline seL4_MessageInfo
seL4_Wait(seL4_CPtr src, seL4_Word* sender)
{
    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
    register seL4_MessageInfo info asm("r1");

    /* Incoming message registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysWait;
    asm volatile ("swi %[swi_num]"
            : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
              "=r" (info), "+r" (src_and_badge)
            : [swi_num] "i" __SWINUM(seL4_SysWait), "r"(scno)
            : "memory");

    /* Write the message back out to memory. */
    seL4_SetMR(0, msg0);
    seL4_SetMR(1, msg1);
    seL4_SetMR(2, msg2);
    seL4_SetMR(3, msg3);

    /* Return back sender and message information. */
    if (sender)
        *sender = src_and_badge;
    return (seL4_MessageInfo)info;
}

static inline seL4_MessageInfo
__seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
    register seL4_MessageInfo info asm("r1");

    /* Incoming message registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysWait;
    asm volatile ("swi %[swi_num]"
            : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
              "=r" (info), "+r" (src_and_badge)
            : [swi_num] "i" __SWINUM(seL4_SysWait), "r"(scno)
            : "memory");

    /* Write the message back out to memory. */
    if (mr0 != NULL) *mr0 = msg0;
    if (mr1 != NULL) *mr1 = msg1;
    if (mr2 != NULL) *mr2 = msg2;
    if (mr3 != NULL) *mr3 = msg3;

    /* Return back sender and message information. */
    if (sender)
        *sender = src_and_badge;
    return (seL4_MessageInfo)info;
}

static inline seL4_MessageInfo
seL4_Poll(seL4_CPtr src, seL4_Word* sender)
{
    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
    register seL4_MessageInfo info asm("r1");

    /* Incoming message registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysPoll;
    asm volatile ("swi %[swi_num]"
            : "=r" (msg0), "=r" (msg1), "=r" (msg2), "=r" (msg3),
              "=r" (info), "+r" (src_and_badge)
            : [swi_num] "i" __SWINUM(seL4_SysPoll), "r"(scno)
            : "memory");

    /* Write the message back out to memory. */
    seL4_SetMR(0, msg0);
    seL4_SetMR(1, msg1);
    seL4_SetMR(2, msg2);
    seL4_SetMR(3, msg3);

    /* Return back sender and message information. */
    if (sender)
        *sender = src_and_badge;
    return (seL4_MessageInfo)info;
}

static inline seL4_MessageInfo
seL4_Call(seL4_CPtr dest, seL4_MessageInfo msgInfo)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_MessageInfo info asm("r1") = msgInfo;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);

    /* Perform the system call. */
    register seL4_Word scno asm("r7") = seL4_SysCall;
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info), "+r" (destptr)
            : [swi_num] "i" __SWINUM(seL4_SysCall), "r"(scno)
            : "memory");

    /* Write out the data back to memory. */
    seL4_SetMR(0, msg0);
    seL4_SetMR(1, msg1);
    seL4_SetMR(2, msg2);
    seL4_SetMR(3, msg3);

    return info;
}

static inline seL4_MessageInfo
__seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo msgInfo,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word destptr asm("r0") = (seL4_Word)dest;
    register seL4_MessageInfo info asm("r1") = msgInfo;

    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");
    register seL4_Word scno asm("r7") = seL4_SysCall;

    /* Load beginning of the message into registers. */
    if (mr0 != NULL && msgInfo.length > 0) { msg0 = *mr0; }
    if (mr1 != NULL && msgInfo.length > 1) { msg1 = *mr1; }
    if (mr2 != NULL && msgInfo.length > 2) { msg2 = *mr2; }
    if (mr3 != NULL && msgInfo.length > 3) { msg3 = *mr3; }

    /* Perform the system call. */
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info), "+r" (destptr)
            : [swi_num] "i" __SWINUM(seL4_SysCall), "r"(scno)
            : "memory");

    /* Write out the data back to memory. */
    if (mr0 != NULL) *mr0 = msg0;
    if (mr1 != NULL) *mr1 = msg1;
    if (mr2 != NULL) *mr2 = msg2;
    if (mr3 != NULL) *mr3 = msg3;

    return info;
}

static inline seL4_MessageInfo
seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo msgInfo, seL4_Word *sender)
{
    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
    register seL4_MessageInfo info asm("r1") = msgInfo;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2") = seL4_GetMR(0);
    register seL4_Word msg1 asm("r3") = seL4_GetMR(1);
    register seL4_Word msg2 asm("r4") = seL4_GetMR(2);
    register seL4_Word msg3 asm("r5") = seL4_GetMR(3);

    /* Perform the syscall. */
    register seL4_Word scno asm("r7") = seL4_SysReplyWait;
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info), "+r" (src_and_badge)
            : [swi_num] "i" __SWINUM(seL4_SysReplyWait), "r"(scno)
            : "memory");

    /* Write the message back out to memory. */
    seL4_SetMR(0, msg0);
    seL4_SetMR(1, msg1);
    seL4_SetMR(2, msg2);
    seL4_SetMR(3, msg3);

    /* Return back sender and message information. */
    if (sender)
        *sender = src_and_badge;
    return info;
}

static inline seL4_MessageInfo
__seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo msgInfo, seL4_Word *sender,
        seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
    register seL4_Word src_and_badge asm("r0") = (seL4_Word)src;
    register seL4_MessageInfo info asm("r1") = msgInfo;

    /* Load beginning of the message into registers. */
    register seL4_Word msg0 asm("r2");
    register seL4_Word msg1 asm("r3");
    register seL4_Word msg2 asm("r4");
    register seL4_Word msg3 asm("r5");
    register seL4_Word scno asm("r7") = seL4_SysReplyWait;

    if (mr0 != NULL && msgInfo.length > 0) { msg0 = *mr0; }
    if (mr1 != NULL && msgInfo.length > 1) { msg1 = *mr1; }
    if (mr2 != NULL && msgInfo.length > 2) { msg2 = *mr2; }
    if (mr3 != NULL && msgInfo.length > 3) { msg3 = *mr3; }

    /* Perform the syscall. */
    asm volatile ("swi %[swi_num]"
            : "+r" (msg0), "+r" (msg1), "+r" (msg2), "+r" (msg3),
              "+r" (info), "+r" (src_and_badge)
            : [swi_num] "i" __SWINUM(seL4_SysReplyWait), "r"(scno)
            : "memory");

    /* Write out the data back to memory. */
    if (mr0 != NULL) *mr0 = msg0;
    if (mr1 != NULL) *mr1 = msg1;
    if (mr2 != NULL) *mr2 = msg2;
    if (mr3 != NULL) *mr3 = msg3;

    /* Return back sender and message information. */
    if (sender)
        *sender = src_and_badge;
    return info;
}

static inline void
seL4_Yield(void) {
    register seL4_Word scno asm("r7") = seL4_SysYield;
    asm volatile ("swi %[swi_num]"
            : /* no outputs */
            : [swi_num] "i" __SWINUM(seL4_SysYield), "r"(scno)
            : "memory");
}

static inline void
seL4_DebugPutChar(char c) {
#ifdef SEL4_DEBUG_KERNEL
    register seL4_Word arg1 asm("r0") = c;
    register seL4_Word scno asm("r7") = seL4_SysDebugPutChar;
    asm volatile ("swi %[swi_num]"
            : /* no outputs */
            : [swi_num] "i" __SWINUM(seL4_SysDebugPutChar), "r" (arg1), "r"(scno));
#endif
}

static inline void
seL4_DebugHalt(void) {
#ifdef SEL4_DEBUG_KERNEL
    register seL4_Word scno asm("r7") = seL4_SysDebugHalt;
    asm volatile ("swi %[swi_num]"
            : /* no outputs */
            : [swi_num] "i" __SWINUM(seL4_SysDebugHalt), "r"(scno));
#endif
}

static inline void
seL4_DebugSnapshot(void) {
#ifdef SEL4_DEBUG_KERNEL
    register seL4_Word scno asm("r7") = seL4_SysDebugSnapshot;
    asm volatile ("swi %[swi_num]"
            : /* no outputs */
            : [swi_num] "i" __SWINUM(seL4_SysDebugSnapshot), "r"(scno));
#endif
}

static inline void
seL4_DebugRun(void (* userfn) (void *), void* userarg) {
#ifdef SEL4_DANGEROUS_CODE_INJECTION_KERNEL
    register seL4_Word arg1 asm("r0") = (seL4_Word)userfn;
    register seL4_Word arg2 asm("r1") = (seL4_Word)userarg;
    register seL4_Word scno asm("r7") = seL4_SysDebugRun;
    asm volatile ("swi %[swi_num]"
            : /* no outputs */
            : [swi_num] "i" __SWINUM(seL4_SysDebugRun), "r" (arg1), "r" (arg2), "r"(scno)
            : "memory"
        );
#endif
}

#undef __SWINUM

#endif
